<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | RunningPRISM / SupportForPEPAModels 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='StartingPRISM.html'>Running PRISM</a> /
</p><h1>Support For PEPA Models</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<p>For CTMCs, PRISM also accepts model descriptions in the stochastic process algebra <a class='urllink' href='http://www.dcs.ed.ac.uk/pepa/'>PEPA</a> [<a class='wikilink' href='../Main/References.html#Hil96'>Hil96</a>].
The tool compiles such descriptions into the PRISM language and then constructs the model as normal.
The language accepted by the PEPA to PRISM compiler is actually a subset of PEPA.
The restrictions applied to the language are firstly that component identifiers can only be bound to sequential components
(formed using prefix and choice and references to other sequential components only).
Secondly, each local state of a  sequential component must be named.  For example, we would rewrite:
</p>
<div class='vspace'></div><ul><li>P = (a,r).(b,s).P;
</li></ul><p class='vspace'>as:
</p>
<div class='vspace'></div><ul><li>P = (a,r).P';
</li><li>P' = (b,s).P;
</li></ul><p class='vspace'>Finally, active/active synchronisations are not allowed since the PRISM 
definition of these differs from the PEPA definition.  Every PEPA 
synchronisation must have exactly one active component.
Some examples of PEPA model descriptions which can be imported into PRISM
can be found in the <code>examples/pepa</code> directory.
</p>
<p class='vspace'>From the command-line version of PRISM, add the <code>-importpepa</code> switch and the model will be treated as a PEPA description.
From the GUI, select "Model | Open model" and then choose "PEPA models"
on the "Files of type" drop-down menu.
Alternatively, select "Model | New | PEPA model" and either type a description from scratch
or paste in an existing one from elsewhere.
Once the PEPA model has been successfully parsed by PRISM,
you can view the corresponding PRISM code (as generated by the PEPA-to-PRISM compiler)
by selecting menu option "Model | View | Parsed PRISM model".
</p>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='../Main/Welcome.html'>PRISM Manual</a></h3>
<p><strong><a class='wikilink' href='StartingPRISM.html'>Running PRISM</a></strong>
</p><ul><li><a class='wikilink' href='StartingPRISM.html'>Starting PRISM</a>
</li><li><a class='wikilink' href='LoadingAndBuildingAModel.html'>Loading And Building a Model</a>
</li><li><a class='wikilink' href='DebuggingModelsWithTheSimulator.html'>Debugging Models With The Simulator</a>
</li><li><a class='wikilink' href='ExportingTheModel.html'>Exporting The Model</a>
</li><li><a class='wikilink' href='ModelChecking.html'>Model Checking</a>
</li><li><a class='wikilink' href='ApproximateModelChecking.html'>Approximate Model Checking</a>
</li><li><a class='wikilink' href='ComputingSteady-stateAndTransientProbabilities.html'>Computing Steady-state And Transient Probabilities</a>
</li><li><a class='wikilink' href='Experiments.html'>Experiments</a>
</li><li><a class='wikilink' href='Adversaries.html'>Adversaries</a>
</li><li><a class='selflink' href='SupportForPEPAModels.html'>Support For PEPA Models</a>
</li><li><a class='wikilink' href='SupportForSBML.html'>Support For SBML</a>
</li><li><a class='wikilink' href='ExplicitModelImport.html'>Explicit Model Import</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
